/-
Copyright (c) 2025 Christian Merten. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Merten
-/
import Mathlib.CategoryTheory.Sites.Precoverage

/-!
# 0-hypercovers

Given a coverage `J` on a category `C`, we define the type
of `0`-hypercovers of an object `S : C`. They consists of a covering family
of morphisms `X i ⟶ S` indexed by a type `I₀` such that the induced presieve is in `J`.

We define this with respect to a coverage and not to a Grothendieck topology, because this
yields more control over the components of the cover.
-/

universe w'' w' w v u

namespace CategoryTheory

open Category Limits

variable {C : Type u} [Category.{v} C]

/-- The categorical data that is involved in a `0`-hypercover of an object `S`. This
consists of a family of morphisms `f i : X i ⟶ S` for `i : I₀`. -/
@[ext]
structure PreZeroHypercover (S : C) where
  /-- the index type of the covering of `S` -/
  I₀ : Type w
  /-- the objects in the covering of `S` -/
  X (i : I₀) : C
  /-- the morphisms in the covering of `S` -/
  f (i : I₀) : X i ⟶ S

namespace PreZeroHypercover

variable {S T : C} (E : PreZeroHypercover.{w} S) (F : PreZeroHypercover.{w'} S)

/-- The assumption that the pullback of `X i₁` and `X i₂` over `S` exists
for any `i₁` and `i₂`. -/
abbrev HasPullbacks := ∀ (i₁ i₂ : E.I₀), HasPullback (E.f i₁) (E.f i₂)

/-- The presieve of `S` that is generated by the morphisms `f i : X i ⟶ S`. -/
abbrev presieve₀ : Presieve S := .ofArrows _ E.f

@[simp]
lemma presieve₀_f (i : E.I₀) : E.presieve₀ (E.f i) := ⟨i⟩

grind_pattern presieve₀_f => E.presieve₀ (E.f i)

/-- The sieve of `S` that is generated by the morphisms `f i : X i ⟶ S`. -/
abbrev sieve₀ : Sieve S := .ofArrows _ E.f

lemma sieve₀_f (i : E.I₀) : E.sieve₀ (E.f i) := ⟨_, 𝟙 _, E.f i, ⟨i⟩, by simp⟩

grind_pattern sieve₀_f => E.sieve₀ (E.f i)

/-- The pre-`0`-hypercover defined by a single morphism. -/
@[simps]
def singleton (f : S ⟶ T) : PreZeroHypercover.{w} T where
  I₀ := PUnit
  X _ := S
  f _ := f

@[simp]
lemma presieve₀_singleton (f : S ⟶ T) : (singleton f).presieve₀ = .singleton f := by
  simp [singleton, presieve₀, Presieve.ofArrows_pUnit]

/-- Pullback of a pre-`0`-hypercover along a morphism. The components are `pullback f (E.f i)`. -/
@[simps]
noncomputable
def pullback₁ (f : S ⟶ T) (E : PreZeroHypercover.{w} T) [∀ i, HasPullback f (E.f i)] :
    PreZeroHypercover.{w} S where
  I₀ := E.I₀
  X i := pullback f (E.f i)
  f _ := pullback.fst _ _

/-- Pullback of a pre-`0`-hypercover along a morphism. The components are `pullback (E.f i) f`. -/
@[simps]
noncomputable
def pullback₂ (f : S ⟶ T) (E : PreZeroHypercover.{w} T) [∀ i, HasPullback (E.f i) f] :
    PreZeroHypercover.{w} S where
  I₀ := E.I₀
  X i := pullback (E.f i) f
  f _ := pullback.snd _ _

lemma presieve₀_pullback₁ (f : S ⟶ T) (E : PreZeroHypercover.{w} T) [∀ i, HasPullback (E.f i) f] :
    presieve₀ (E.pullback₂ f) = E.presieve₀.pullbackArrows f := by
  refine le_antisymm ?_ ?_
  · rintro - - ⟨i⟩
    use _, _, i
  · rintro W g ⟨-, -, ⟨i⟩⟩
    use i

/-- Refining each component of a pre-`0`-hypercover yields a refined pre-`0`-hypercover of the
base. -/
@[simps]
def bind (E : PreZeroHypercover.{w} T) (F : ∀ i, PreZeroHypercover.{w'} (E.X i)) :
    PreZeroHypercover.{max w w'} T where
  I₀ := Σ (i : E.I₀), (F i).I₀
  X ij := (F ij.1).X ij.2
  f ij := (F ij.1).f ij.2 ≫ E.f ij.1

/-- Replace the indexing type of a pre-`0`-hypercover. -/
@[simps]
def reindex (E : PreZeroHypercover.{w} T) {ι : Type w'} (e : ι ≃ E.I₀) :
    PreZeroHypercover.{w'} T where
  I₀ := ι
  X := E.X ∘ e
  f i := E.f (e i)

@[simp]
lemma presieve₀_reindex {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).presieve₀ = E.presieve₀ := by
  refine le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_
  obtain ⟨i, rfl⟩ := e.surjective i
  exact ⟨i⟩

/-- Pairwise intersection of two pre-`0`-hypercovers. -/
@[simps!]
noncomputable
def inter (E : PreZeroHypercover.{w} T) (F : PreZeroHypercover.{w'} T)
    [∀ i j, HasPullback (E.f i) (F.f j)] :
    PreZeroHypercover.{max w w'} T :=
  (E.bind (fun i ↦ F.pullback₁ (E.f i))).reindex (Equiv.sigmaEquivProd _ _).symm

lemma inter_def [∀ i j, HasPullback (E.f i) (F.f j)] :
    E.inter F = (E.bind (fun i ↦ F.pullback₁ (E.f i))).reindex (Equiv.sigmaEquivProd _ _).symm :=
  rfl

/-- Disjoint union of two pre-`0`-hypercovers. -/
@[simps I₀, simps -isSimp X f]
def sum {X : C} (E : PreZeroHypercover.{w} X) (F : PreZeroHypercover.{w'} X) :
    PreZeroHypercover.{max w w'} X where
  I₀ := E.I₀ ⊕ F.I₀
  X := Sum.elim E.X F.X
  f
    | .inl i => E.f i
    | .inr i => F.f i

@[simp] lemma sum_X_inl (i : E.I₀) : (E.sum F).X (.inl i) = E.X i := rfl

@[simp] lemma sum_X_inr (i : F.I₀) : (E.sum F).X (.inr i) = F.X i := rfl

@[simp] lemma sum_f_inl (i : E.I₀) : (E.sum F).f (.inl i) = E.f i := rfl

@[simp] lemma sum_f_inr (i : F.I₀) : (E.sum F).f (.inr i) = F.f i := rfl

@[simp]
lemma presieve₀_sum : (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀ := by
  rw [presieve₀, presieve₀, presieve₀]
  apply le_antisymm
  · intro Z g ⟨i⟩
    cases i
    · exact Or.inl (.mk _)
    · exact Or.inr (.mk _)
  · rintro Z g (⟨⟨i⟩⟩|⟨⟨i⟩⟩)
    · exact ⟨Sum.inl i⟩
    · exact ⟨Sum.inr i⟩

/-- Add a morphism to a pre-`0`-hypercover. -/
@[simps! I₀]
def add (E : PreZeroHypercover.{w} S) {T : C} (f : T ⟶ S) : PreZeroHypercover.{w} S :=
  (E.sum (.singleton f)).reindex (Equiv.optionEquivSumPUnit.{0} E.I₀)

@[simp] lemma add_X_some {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).X (some i) = E.X i := rfl

@[simp] lemma add_X_none {T : C} (f : T ⟶ S) : (E.add f).X none = T := rfl

@[simp] lemma add_f_some {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).f (some i) = E.f i := rfl

@[simp] lemma add_f_nome {T : C} (f : T ⟶ S) : (E.add f).f none = f := rfl

@[simp] lemma presieve₀_add {T : C} (f : T ⟶ S) :
    (E.add f).presieve₀ = E.presieve₀ ⊔ .singleton f := by
  simp [add, presieve₀_reindex, presieve₀_sum]

section Category

variable {E : PreZeroHypercover.{w} S} {F : PreZeroHypercover.{w'} S}

/-- A morphism of pre-`0`-hypercovers of `S` is a family of refinement morphisms commuting
with the structure morphisms of `E` and `F`. -/
@[ext]
structure Hom (E : PreZeroHypercover.{w} S) (F : PreZeroHypercover.{w'} S) where
  /-- The map between indexing types of the coverings of `S` -/
  s₀ (i : E.I₀) : F.I₀
  /-- The refinement morphisms between objects in the coverings of `S`. -/
  h₀ (i : E.I₀) : E.X i ⟶ F.X (s₀ i)
  w₀ (i : E.I₀) : h₀ i ≫ F.f (s₀ i) = E.f i := by cat_disch

attribute [reassoc (attr := simp)] Hom.w₀

/-- The identity refinement of a pre-`0`-hypercover. -/
@[simps]
def Hom.id (E : PreZeroHypercover S) : Hom E E where
  s₀ := _root_.id
  h₀ _ := 𝟙 _

variable {G : PreZeroHypercover S}

/-- Composition of refinement morphisms of pre-`0`-hypercovers. -/
@[simps]
def Hom.comp (f : E.Hom F) (g : F.Hom G) : E.Hom G where
  s₀ := g.s₀ ∘ f.s₀
  h₀ i := f.h₀ i ≫ g.h₀ _

@[simps! id_s₀ id_h₀ comp_s₀ comp_h₀]
instance : Category (PreZeroHypercover S) where
  Hom := Hom
  id E := Hom.id E
  comp f g := f.comp g

end Category

section Functoriality

variable {D : Type*} [Category D] {F : C ⥤ D}

/-- The image of a pre-`0`-hypercover under a functor. -/
@[simps]
def map (F : C ⥤ D) (E : PreZeroHypercover.{w} S) : PreZeroHypercover.{w} (F.obj S) where
  I₀ := E.I₀
  X i := F.obj (E.X i)
  f i := F.map (E.f i)

lemma presieve₀_map : (E.map F).presieve₀ = E.presieve₀.map F :=
  (Presieve.map_ofArrows _).symm

end Functoriality

section

variable (F : PreZeroHypercover.{w'} S) {G : PreZeroHypercover.{w''} S}

/-- The left inclusion into the disjoint union. -/
@[simps]
def sumInl : E.Hom (E.sum F) where
  s₀ := Sum.inl
  h₀ _ := 𝟙 _

/-- The right inclusion into the disjoint union. -/
@[simps]
def sumInr : F.Hom (E.sum F) where
  s₀ := Sum.inr
  h₀ _ := 𝟙 _

variable {E F} in
/-- To give a refinement of the disjoint union, it suffices to give refinements of both
components. -/
@[simps]
def sumLift (f : E.Hom G) (g : F.Hom G) : (E.sum F).Hom G where
  s₀ := Sum.elim f.s₀ g.s₀
  h₀
    | .inl i => f.h₀ i
    | .inr i => g.h₀ i

variable [∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)]

/-- First projection from the intersection of two pre-`0`-hypercovers. -/
@[simps]
noncomputable
def interFst : Hom (inter E F) E where
  s₀ i := i.1
  h₀ _ := pullback.fst _ _

/-- Second projection from the intersection of two pre-`0`-hypercovers. -/
@[simps]
noncomputable
def interSnd : Hom (inter E F) F where
  s₀ i := i.2
  h₀ _ := pullback.snd _ _
  w₀ i := by simp [← pullback.condition]

variable {E F} in
/-- Universal property of the intersection of two pre-`0`-hypercovers. -/
@[simps]
noncomputable
def interLift (f : G.Hom E) (g : G.Hom F) :
    G.Hom (E.inter F) where
  s₀ i := ⟨f.s₀ i, g.s₀ i⟩
  h₀ i := pullback.lift (f.h₀ i) (g.h₀ i) (by simp)

end

end PreZeroHypercover

namespace Precoverage

variable {J : Precoverage C}

/-- The type of `0`-hypercovers of an object `S : C` in a category equipped with a
coverage `J`. This can be constructed from a covering of `S`. -/
structure ZeroHypercover (J : Precoverage C) (S : C) extends PreZeroHypercover.{w} S where
  mem₀ : toPreZeroHypercover.presieve₀ ∈ J S

namespace ZeroHypercover

variable {S T : C}

/-- The `0`-hypercover defined by a single covering morphism. -/
@[simps toPreZeroHypercover]
def singleton (f : S ⟶ T) (hf : Presieve.singleton f ∈ J T) :
    J.ZeroHypercover T where
  __ := PreZeroHypercover.singleton f
  mem₀ := by
    simpa [PreZeroHypercover.presieve₀, PreZeroHypercover.singleton, Presieve.ofArrows_pUnit]

/-- Pullback of a `0`-hypercover along a morphism. The components are `pullback f (E.f i)`. -/
@[simps toPreZeroHypercover]
noncomputable
def pullback₁ [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : ZeroHypercover.{w} J T)
    [∀ i, HasPullback f (E.f i)] : J.ZeroHypercover S where
  __ := E.toPreZeroHypercover.pullback₁ f
  mem₀ := J.mem_coverings_of_isPullback E.f E.mem₀ f _
    (fun _ ↦ pullback.snd _ _) fun i ↦ IsPullback.of_hasPullback f (E.f i)

/-- Pullback of a `0`-hypercover along a morphism. The components are `pullback (E.f i) f`. -/
@[simps toPreZeroHypercover]
noncomputable
def pullback₂ [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : ZeroHypercover.{w} J T)
    [∀ i, HasPullback (E.f i) f] : J.ZeroHypercover S where
  __ := E.toPreZeroHypercover.pullback₂ f
  mem₀ := J.mem_coverings_of_isPullback E.f E.mem₀ f _
    (fun _ ↦ pullback.fst _ _) fun i ↦ (IsPullback.of_hasPullback (E.f i) f).flip

/-- Refining each component of a `0`-hypercover yields a refined `0`-hypercover of the base. -/
@[simps toPreZeroHypercover]
def bind [J.IsStableUnderComposition] (E : ZeroHypercover.{w} J T)
    (F : ∀ i, ZeroHypercover.{w'} J (E.X i)) :
    ZeroHypercover.{max w w'} J T where
  __ := E.toPreZeroHypercover.bind (fun i ↦ (F i).toPreZeroHypercover)
  mem₀ :=
    comp_mem_coverings (f := E.f) (g := fun i j ↦ (F i).f j) E.mem₀ (fun i ↦ (F i).mem₀)

/-- Pairwise intersection of two `0`-hypercovers. -/
@[simps toPreZeroHypercover]
noncomputable
def inter [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : ZeroHypercover.{w} J T)
    (F : ZeroHypercover.{w'} J T) [∀ i j, HasPullback (E.f i) (F.f j)] :
    ZeroHypercover.{max w w'} J T where
  __ := E.toPreZeroHypercover.inter F.toPreZeroHypercover
  mem₀ := by
    rw [PreZeroHypercover.inter_def, PreZeroHypercover.presieve₀_reindex]
    exact (E.bind (fun i ↦ F.pullback₁ (E.f i))).mem₀

/-- Replace the indexing type of a `0`-hypercover. -/
@[simps toPreZeroHypercover]
def reindex (E : ZeroHypercover.{w} J T) {ι : Type w'} (e : ι ≃ E.I₀) :
    ZeroHypercover.{w'} J T where
  __ := E.toPreZeroHypercover.reindex e
  mem₀ := by simp [E.mem₀]

/-- Disjoint union of two `0`-hypercovers. -/
@[simps toPreZeroHypercover]
def sum [J.IsStableUnderSup] (E : ZeroHypercover.{w} J S) (F : ZeroHypercover.{w'} J S) :
    ZeroHypercover.{max w w'} J S where
  __ := E.toPreZeroHypercover.sum F.toPreZeroHypercover
  mem₀ := by
    rw [PreZeroHypercover.presieve₀_sum]
    exact J.sup_mem_coverings E.mem₀ F.mem₀

/-- Add a single morphism to a `0`-hypercover. -/
@[simps toPreZeroHypercover]
def add (E : ZeroHypercover.{w} J S) {T : C} (f : T ⟶ S)
    (hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J S) :
    ZeroHypercover.{w} J S where
  __ := E.toPreZeroHypercover.add f
  mem₀ := by rwa [PreZeroHypercover.presieve₀_add]

/-- If `L` is a finer precoverage than `K`, any `0`-hypercover wrt. `K` is in particular
a `0`-hypercover wrt. to `L`. -/
@[simps toPreZeroHypercover]
def weaken {K L : Precoverage C} {X : C} (E : Precoverage.ZeroHypercover K X) (h : K ≤ L) :
    Precoverage.ZeroHypercover L X where
  __ := E
  mem₀ := h _ E.mem₀

instance (K : Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) :
    E.presieve₀.HasPullbacks f :=
  K.hasPullbacks_of_mem _ E.mem₀

instance {X Y : C} (E : PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f]
    (i : E.I₀) : HasPullback (E.f i) f :=
  E.presieve₀.hasPullback f ⟨i⟩

instance {X Y : C} (E : PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f]
    (i : E.I₀) : HasPullback f (E.f i) :=
  hasPullback_symmetry (E.f i) f

variable (J) in
/-- A morphism of `0`-hypercovers is a morphism of the underlying pre-`0`-hypercovers. -/
abbrev Hom (E : ZeroHypercover.{w} J S) (F : ZeroHypercover.{w'} J S) :=
  E.toPreZeroHypercover.Hom F.toPreZeroHypercover

@[simps! id_s₀ id_h₀ comp_s₀ comp_h₀]
instance : Category (ZeroHypercover.{w} J S) where
  Hom := Hom J
  id _ := PreZeroHypercover.Hom.id _
  comp := PreZeroHypercover.Hom.comp

section Functoriality

variable {D : Type*} [Category D] {F : C ⥤ D} {K : Precoverage D}

/-- The image of a `0`-hypercover under a functor. -/
@[simps toPreZeroHypercover]
def map (F : C ⥤ D) (E : ZeroHypercover.{w} J S) (h : J ≤ K.comap F) :
    ZeroHypercover.{w} K (F.obj S) where
  __ := E.toPreZeroHypercover.map F
  mem₀ := by
    rw [PreZeroHypercover.presieve₀_map, ← mem_comap_iff]
    exact h _ E.mem₀

end Functoriality

end ZeroHypercover

lemma mem_iff_exists_zeroHypercover {X : C} {R : Presieve X} :
    R ∈ J X ↔ ∃ (𝒰 : ZeroHypercover.{max u v} J X), R = Presieve.ofArrows 𝒰.X 𝒰.f := by
  refine ⟨fun hR ↦ ?_, fun ⟨𝒰, hR⟩ ↦ hR ▸ 𝒰.mem₀⟩
  obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
  use ⟨⟨ι, Y, f⟩, hR⟩

end Precoverage

end CategoryTheory
